(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const _22-0 (_ BitVec 22))
(assert (= v13 v8 v13 (= v12 v1 v0 v2 v2 v11 v1 v7) v14))
(assert v2)
(assert v8)
(check-sat)
